Inference at * 2 1 2 1 1 
Iof proof for Lemma before last:



1. T : Type
2. T List
3. u : T
4. v : T List
5. x:T. (x  v)  ((x = last(v)))  x before last(v)  v
6. x : T
7. x = u
8. v = []
9. z : T List
  (null([u / z])) 

latex

 by ((Reduce 0) 
CollapseTHEN (SimpConcl)) 

latex

C.

Definitions	t  T, True, if b then t else f fi , ff, null(as), b, A, P  Q,
Lemmas	false wf